i:Id, da:k:{k:Knd| hasloc(k;i)}  fp :Type{i}  Top. normal-ma-da{i:l}(da)  {i'} 

latex

Definitions	Id, t  T, Top, Type, x:A  B(x), x:A. B(x), Knd, b, {x:A| B(x)} , (x  l), x:AB(x), hasloc(k;i), type List, Atom$n, P  Q, x. t(x), f(x), t.1, Normal(T), a:A fp B(a), let x,y = A in B(x;y), f(a), left + right, if b then t else f fi , Void, x:A.B(x), <a, b>, s = t, S  T, , x.A(x), IdLnk, KindDeq, x  dom(f), , Normal(da)
Lemmas	Kind-deq wf, IdLnk wf, fpf-dom wf, subtype rel product, subtype rel list, subtype rel function, subtype rel set, subtype-set-hasloc, fpf-trivial-subtype-set, fpf-trivial-subtype-top, normal-type wf, pi1 wf, fpf-ap wf, Knd wf, assert wf, hasloc wf, l member wf, top wf, Id wf